Lean4 Metaprogramming Book
Sect 2.
SyntaxとExprの違い/相互性を見る
https://user-images.githubusercontent.com/7578559/246022611-78867009-2624-46a3-a1f4-f488fd25d494.png
ステップ
1. Parsing
文字列をSyntaxに変換する："let a := 2" → Syntax
関わってくるのはSyntax
2. Elaborating：Syntax→Syntax
Syntaxに全てのMacroを適用する
3. Finally：Syntax→Expr
Finally, it's time to infuse your syntax with meaning - Lean finds an elab that's matched to the appropriate syntax rule by the :name argument (syntax rules, macros and elabs all have this argument, and they must match). The newfound elab returns a particular Expr object. This completes the elaboration step.
Elaboratingとはtaking a partially-specified expression and inferring what is left implicitのことを指す．
評価中に一旦穴(Hole)を開けておいて，後で推論する，みたいな気持ちか？
https://user-images.githubusercontent.com/7578559/246744085-9b83f06c-49c4-4d93-9d42-72e0499ae6c8.png
notation, prefix, infix, postfixはsyntaxと@[macro xxx] def ourMacroの組み合わせである．
https://user-images.githubusercontent.com/7578559/246751716-adc1284f-3c0a-441d-91b8-7d87b6035688.png
#h "#explode"または#help "#explode"と書くと，#explodeコマンドの素朴なFitch流証明図を出す #h "#explide"
→ syntax (name := shortcut_h)で検知
→ @[macro shortcut_h] def helpMacroで#helpに書き換える
→ syntax (name := default_h)で検知
→ @[command_elab default_h] def helpElab
Syntax Rule，Macro，Elabsはname属性で検知することに注意．
#helpではCommandElabを用いたが，Elab Functionには別の種類もある
TermElab．Syntax → Option Expr → TermElabM Expr
Exprオブジェクトを返すことが期待される．
CommandElab．Syntax → CommandElabM Unit．何も返さない．
Tactic．Syntax → TacticM Unit．同様に何も返さない．
code:sect2_1.lean
import Lean
open Lean Elab Command
syntax (name := xxx) "red" : command
syntax (name := yyy) "green" : command
syntax (name := zzz) "blue" : command
match stx with
| _ => `(green)
@macro yyy def greenMacro : Macro := λ stx => match stx with
| _ => `(blue)
Lean.logInfo "finally, blue!"
red -- finally, blue!
最後の行のredについて
1. syntax (name := xxx) "red" : commandで検知され，xxxという名前のMacroかElabを探す．
2. redMacroというMacroがxxxとして引っかかる．ここでgreenに置換される．
3. syntax (name := yyy) "green" : commandで検知され，yyyという名前のMacroかElabを探す．
4. greenMacroというMacroがyyyとして引っかかる．ここでblueに置換される．
5. syntax (name := zzz) "blue" : commandで検知され，zzzという名前のMacroかElabを探す．
6. Macroは無いので，blueElabというElabが引っかかる．"finally, blue!"というログを吐き出す．
In principle, you can do with a macro (almost?) anything you can do with the elab function. Just write what you would have in the body of your elab as a syntax within macro. However, the rule of thumb here is to only use macros when the conversion is simple and truly feels elementary to the point of aliasing.
As Henrik Böving puts it:
"as soon as types or control flow is involved a macro is probably not reasonable anymore" (Zulip thread).
So - use macros for creating syntax sugars, notations, and shortcuts, and prefer elabs for writing out code with some programming logic, even if it's potentially implementable in a macro.
dbg_traceというのを使ってデバッグするのも手
Sect 3. Expressions
Exprについて
The ultimate purpose of a Lean tactic block is to generate a term which serves as a proof of the theorem we want to prove. Thus, the purpose of a tactic is to produce (part of) an Expr of the right type. Much metaprogramming therefore comes down to manipulating expressions: constructing new ones and taking apart existing ones.
究極的にはLeanでの証明とは，証明したい項を生成することに尽きる．
Tacticは適切な項を生成する．
Sect4. MetaM
CoreM: EnvironmentにアクセするためのMonad
Environmentというのは例えば現時点で宣言されているものとかimportされているものとか
MetaM: メタ変数のコンテクストにアクセスするためのMonad. 現状宣言されてvalueがassignされてるメタ変数について
TermElabM: Elaboration中に詳細情報にアクセスするために
TacticM: 現状のゴールにアクセスするためのMonad
メタ変数を普通は扱わないが見るだけならある
goalとして
code:sect4_goal
n m : Nat
⊢ n + m = m + n
holeとしてEq.transによって↓が生成のgoalが生成される．
code:sect4_hole
n m : Nat
⊢ n = ?x
n m : Nat
⊢ ?x = m
このとき?xは[n : Nat, m : Nat]というlocal contextを持つ．
上の例では?x := nとすればよい．
code:sect4_example_1
example {α} (a : α) (f : α → α) (h : ∀ a, f a = a) : f (f a) = a := by
apply Eq.trans
apply h
apply h
Eq.transをapplyした時点でのゴール/メタ変数
$ f (f a) = ?b
$ ?b = a
$ α